$\forall$${\it es}$:ES, ${\it e'}$:E, $P$:(\{$e$:E$\mid$ loc($e$) $=$ loc(${\it e'}$) $\in$ Id \}$\rightarrow$Prop).
\\[0ex]($\forall$$e$$<$${\it e'}$. $P$($e$)) $\Leftrightarrow$ ($\neg$first(${\it e'}$) $\Rightarrow$ $P$(pred(${\it e'}$)) \& ($\forall$$e$$<$pred(${\it e'}$). $P$($e$)))